D:Dsys.
Feasible(D)  (l:IdLnk, tg:Id. M(source(l)).dout(l,tg)  M(destination(l)).din(l,tg)) 

latex

Definitions	t  T, x:A. B(x), False, P  Q, A, M.din(l,tg), M(i), M.dout(l,tg), Id, s = t, Prop, b, Type, b, , a = b, x:AB(x), x:AB(x), P & Q, P  Q, {T}, SQType(T), s ~ t, left+right, P  Q, Dsys, Feasible(D), IdLnk, destination(l)
Lemmas	IdLnk wf, d-feasible wf, dsys wf, d-feasible-types, bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, Id wf, ldst wf